es:ES, e, e':E. (loc(e) = loc(e')  Id)  (es-init(es;e) = es-init(es;e')  E) 

latex

Definitions	left + right, P  Q, x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, t  T, x:A. B(x), es-init(es;e), <a, b>, E, s = t, Id, (e <loc e'), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, b, t.1, P  Q, A, Void, False, pred(e), (e < e'), x,y. t(x;y), let x,y = A in B(x;y), loc(e), SQType(T), , s ~ t, Atom$n, isrcv(e), Type, True, T
Lemmas	es-init wf, squash wf, true wf, es-pred-locl, es-isrcv-loc, es-le-loc, Id sq, es-loc-pred, all functionality wrt iff, implies functionality wrt iff, wellfounded functionality wrt iff, es-init-elim2, es-locl-iff, es-pred wf, es-locl-wellfnd, es-axioms